$\forall$${\it ds}$, ${\it ds'}$:$x$:Id fp$\rightarrow$ Type, $T$:Type. ${\it ds}$ $\subseteq$ ${\it ds'}$ $\Rightarrow$ (State(${\it ds'}$) $\subseteq$r State(${\it ds}$))